0 Prolog
↳1 PrologToPiTRSProof (⇒, 61 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 93 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 4 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 QDPQMonotonicMRRProof (⇔, 223 ms)
↳34 QDP
↳35 Narrowing (⇒, 1 ms)
↳36 QDP
↳37 DependencyGraphProof (⇔, 0 ms)
↳38 TRUE
gcd_in_gga(X, Y, D) → U1_gga(X, Y, D, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg(0, s(Y))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(X, Y, D, le_out_gg(X, Y)) → U2_gga(X, Y, D, gcd_le_in_gga(X, Y, D))
gcd_le_in_gga(0, Y, Y) → gcd_le_out_gga(0, Y, Y)
gcd_le_in_gga(s(X), Y, D) → U5_gga(X, Y, D, add_in_gag(s(X), Z, Y))
add_in_gag(s(X), Y, s(Z)) → U9_gag(X, Y, Z, add_in_gag(X, Y, Z))
add_in_gag(0, X, X) → add_out_gag(0, X, X)
U9_gag(X, Y, Z, add_out_gag(X, Y, Z)) → add_out_gag(s(X), Y, s(Z))
U5_gga(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_gga(X, Y, D, gcd_in_gga(s(X), Z, D))
gcd_in_gga(X, Y, D) → U3_gga(X, Y, D, gt_in_gg(X, Y))
gt_in_gg(s(X), s(Y)) → U7_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg(s(X), 0)
U7_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(X, Y, D, gt_out_gg(X, Y)) → U4_gga(X, Y, D, gcd_le_in_gga(Y, X, D))
U4_gga(X, Y, D, gcd_le_out_gga(Y, X, D)) → gcd_out_gga(X, Y, D)
U6_gga(X, Y, D, gcd_out_gga(s(X), Z, D)) → gcd_le_out_gga(s(X), Y, D)
U2_gga(X, Y, D, gcd_le_out_gga(X, Y, D)) → gcd_out_gga(X, Y, D)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
gcd_in_gga(X, Y, D) → U1_gga(X, Y, D, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg(0, s(Y))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(X, Y, D, le_out_gg(X, Y)) → U2_gga(X, Y, D, gcd_le_in_gga(X, Y, D))
gcd_le_in_gga(0, Y, Y) → gcd_le_out_gga(0, Y, Y)
gcd_le_in_gga(s(X), Y, D) → U5_gga(X, Y, D, add_in_gag(s(X), Z, Y))
add_in_gag(s(X), Y, s(Z)) → U9_gag(X, Y, Z, add_in_gag(X, Y, Z))
add_in_gag(0, X, X) → add_out_gag(0, X, X)
U9_gag(X, Y, Z, add_out_gag(X, Y, Z)) → add_out_gag(s(X), Y, s(Z))
U5_gga(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_gga(X, Y, D, gcd_in_gga(s(X), Z, D))
gcd_in_gga(X, Y, D) → U3_gga(X, Y, D, gt_in_gg(X, Y))
gt_in_gg(s(X), s(Y)) → U7_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg(s(X), 0)
U7_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(X, Y, D, gt_out_gg(X, Y)) → U4_gga(X, Y, D, gcd_le_in_gga(Y, X, D))
U4_gga(X, Y, D, gcd_le_out_gga(Y, X, D)) → gcd_out_gga(X, Y, D)
U6_gga(X, Y, D, gcd_out_gga(s(X), Z, D)) → gcd_le_out_gga(s(X), Y, D)
U2_gga(X, Y, D, gcd_le_out_gga(X, Y, D)) → gcd_out_gga(X, Y, D)
GCD_IN_GGA(X, Y, D) → U1_GGA(X, Y, D, le_in_gg(X, Y))
GCD_IN_GGA(X, Y, D) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → U8_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U1_GGA(X, Y, D, le_out_gg(X, Y)) → U2_GGA(X, Y, D, gcd_le_in_gga(X, Y, D))
U1_GGA(X, Y, D, le_out_gg(X, Y)) → GCD_LE_IN_GGA(X, Y, D)
GCD_LE_IN_GGA(s(X), Y, D) → U5_GGA(X, Y, D, add_in_gag(s(X), Z, Y))
GCD_LE_IN_GGA(s(X), Y, D) → ADD_IN_GAG(s(X), Z, Y)
ADD_IN_GAG(s(X), Y, s(Z)) → U9_GAG(X, Y, Z, add_in_gag(X, Y, Z))
ADD_IN_GAG(s(X), Y, s(Z)) → ADD_IN_GAG(X, Y, Z)
U5_GGA(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_GGA(X, Y, D, gcd_in_gga(s(X), Z, D))
U5_GGA(X, Y, D, add_out_gag(s(X), Z, Y)) → GCD_IN_GGA(s(X), Z, D)
GCD_IN_GGA(X, Y, D) → U3_GGA(X, Y, D, gt_in_gg(X, Y))
GCD_IN_GGA(X, Y, D) → GT_IN_GG(X, Y)
GT_IN_GG(s(X), s(Y)) → U7_GG(X, Y, gt_in_gg(X, Y))
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
U3_GGA(X, Y, D, gt_out_gg(X, Y)) → U4_GGA(X, Y, D, gcd_le_in_gga(Y, X, D))
U3_GGA(X, Y, D, gt_out_gg(X, Y)) → GCD_LE_IN_GGA(Y, X, D)
gcd_in_gga(X, Y, D) → U1_gga(X, Y, D, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg(0, s(Y))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(X, Y, D, le_out_gg(X, Y)) → U2_gga(X, Y, D, gcd_le_in_gga(X, Y, D))
gcd_le_in_gga(0, Y, Y) → gcd_le_out_gga(0, Y, Y)
gcd_le_in_gga(s(X), Y, D) → U5_gga(X, Y, D, add_in_gag(s(X), Z, Y))
add_in_gag(s(X), Y, s(Z)) → U9_gag(X, Y, Z, add_in_gag(X, Y, Z))
add_in_gag(0, X, X) → add_out_gag(0, X, X)
U9_gag(X, Y, Z, add_out_gag(X, Y, Z)) → add_out_gag(s(X), Y, s(Z))
U5_gga(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_gga(X, Y, D, gcd_in_gga(s(X), Z, D))
gcd_in_gga(X, Y, D) → U3_gga(X, Y, D, gt_in_gg(X, Y))
gt_in_gg(s(X), s(Y)) → U7_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg(s(X), 0)
U7_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(X, Y, D, gt_out_gg(X, Y)) → U4_gga(X, Y, D, gcd_le_in_gga(Y, X, D))
U4_gga(X, Y, D, gcd_le_out_gga(Y, X, D)) → gcd_out_gga(X, Y, D)
U6_gga(X, Y, D, gcd_out_gga(s(X), Z, D)) → gcd_le_out_gga(s(X), Y, D)
U2_gga(X, Y, D, gcd_le_out_gga(X, Y, D)) → gcd_out_gga(X, Y, D)
GCD_IN_GGA(X, Y, D) → U1_GGA(X, Y, D, le_in_gg(X, Y))
GCD_IN_GGA(X, Y, D) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → U8_GG(X, Y, le_in_gg(X, Y))
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
U1_GGA(X, Y, D, le_out_gg(X, Y)) → U2_GGA(X, Y, D, gcd_le_in_gga(X, Y, D))
U1_GGA(X, Y, D, le_out_gg(X, Y)) → GCD_LE_IN_GGA(X, Y, D)
GCD_LE_IN_GGA(s(X), Y, D) → U5_GGA(X, Y, D, add_in_gag(s(X), Z, Y))
GCD_LE_IN_GGA(s(X), Y, D) → ADD_IN_GAG(s(X), Z, Y)
ADD_IN_GAG(s(X), Y, s(Z)) → U9_GAG(X, Y, Z, add_in_gag(X, Y, Z))
ADD_IN_GAG(s(X), Y, s(Z)) → ADD_IN_GAG(X, Y, Z)
U5_GGA(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_GGA(X, Y, D, gcd_in_gga(s(X), Z, D))
U5_GGA(X, Y, D, add_out_gag(s(X), Z, Y)) → GCD_IN_GGA(s(X), Z, D)
GCD_IN_GGA(X, Y, D) → U3_GGA(X, Y, D, gt_in_gg(X, Y))
GCD_IN_GGA(X, Y, D) → GT_IN_GG(X, Y)
GT_IN_GG(s(X), s(Y)) → U7_GG(X, Y, gt_in_gg(X, Y))
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
U3_GGA(X, Y, D, gt_out_gg(X, Y)) → U4_GGA(X, Y, D, gcd_le_in_gga(Y, X, D))
U3_GGA(X, Y, D, gt_out_gg(X, Y)) → GCD_LE_IN_GGA(Y, X, D)
gcd_in_gga(X, Y, D) → U1_gga(X, Y, D, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg(0, s(Y))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(X, Y, D, le_out_gg(X, Y)) → U2_gga(X, Y, D, gcd_le_in_gga(X, Y, D))
gcd_le_in_gga(0, Y, Y) → gcd_le_out_gga(0, Y, Y)
gcd_le_in_gga(s(X), Y, D) → U5_gga(X, Y, D, add_in_gag(s(X), Z, Y))
add_in_gag(s(X), Y, s(Z)) → U9_gag(X, Y, Z, add_in_gag(X, Y, Z))
add_in_gag(0, X, X) → add_out_gag(0, X, X)
U9_gag(X, Y, Z, add_out_gag(X, Y, Z)) → add_out_gag(s(X), Y, s(Z))
U5_gga(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_gga(X, Y, D, gcd_in_gga(s(X), Z, D))
gcd_in_gga(X, Y, D) → U3_gga(X, Y, D, gt_in_gg(X, Y))
gt_in_gg(s(X), s(Y)) → U7_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg(s(X), 0)
U7_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(X, Y, D, gt_out_gg(X, Y)) → U4_gga(X, Y, D, gcd_le_in_gga(Y, X, D))
U4_gga(X, Y, D, gcd_le_out_gga(Y, X, D)) → gcd_out_gga(X, Y, D)
U6_gga(X, Y, D, gcd_out_gga(s(X), Z, D)) → gcd_le_out_gga(s(X), Y, D)
U2_gga(X, Y, D, gcd_le_out_gga(X, Y, D)) → gcd_out_gga(X, Y, D)
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
gcd_in_gga(X, Y, D) → U1_gga(X, Y, D, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg(0, s(Y))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(X, Y, D, le_out_gg(X, Y)) → U2_gga(X, Y, D, gcd_le_in_gga(X, Y, D))
gcd_le_in_gga(0, Y, Y) → gcd_le_out_gga(0, Y, Y)
gcd_le_in_gga(s(X), Y, D) → U5_gga(X, Y, D, add_in_gag(s(X), Z, Y))
add_in_gag(s(X), Y, s(Z)) → U9_gag(X, Y, Z, add_in_gag(X, Y, Z))
add_in_gag(0, X, X) → add_out_gag(0, X, X)
U9_gag(X, Y, Z, add_out_gag(X, Y, Z)) → add_out_gag(s(X), Y, s(Z))
U5_gga(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_gga(X, Y, D, gcd_in_gga(s(X), Z, D))
gcd_in_gga(X, Y, D) → U3_gga(X, Y, D, gt_in_gg(X, Y))
gt_in_gg(s(X), s(Y)) → U7_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg(s(X), 0)
U7_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(X, Y, D, gt_out_gg(X, Y)) → U4_gga(X, Y, D, gcd_le_in_gga(Y, X, D))
U4_gga(X, Y, D, gcd_le_out_gga(Y, X, D)) → gcd_out_gga(X, Y, D)
U6_gga(X, Y, D, gcd_out_gga(s(X), Z, D)) → gcd_le_out_gga(s(X), Y, D)
U2_gga(X, Y, D, gcd_le_out_gga(X, Y, D)) → gcd_out_gga(X, Y, D)
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
GT_IN_GG(s(X), s(Y)) → GT_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
ADD_IN_GAG(s(X), Y, s(Z)) → ADD_IN_GAG(X, Y, Z)
gcd_in_gga(X, Y, D) → U1_gga(X, Y, D, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg(0, s(Y))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(X, Y, D, le_out_gg(X, Y)) → U2_gga(X, Y, D, gcd_le_in_gga(X, Y, D))
gcd_le_in_gga(0, Y, Y) → gcd_le_out_gga(0, Y, Y)
gcd_le_in_gga(s(X), Y, D) → U5_gga(X, Y, D, add_in_gag(s(X), Z, Y))
add_in_gag(s(X), Y, s(Z)) → U9_gag(X, Y, Z, add_in_gag(X, Y, Z))
add_in_gag(0, X, X) → add_out_gag(0, X, X)
U9_gag(X, Y, Z, add_out_gag(X, Y, Z)) → add_out_gag(s(X), Y, s(Z))
U5_gga(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_gga(X, Y, D, gcd_in_gga(s(X), Z, D))
gcd_in_gga(X, Y, D) → U3_gga(X, Y, D, gt_in_gg(X, Y))
gt_in_gg(s(X), s(Y)) → U7_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg(s(X), 0)
U7_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(X, Y, D, gt_out_gg(X, Y)) → U4_gga(X, Y, D, gcd_le_in_gga(Y, X, D))
U4_gga(X, Y, D, gcd_le_out_gga(Y, X, D)) → gcd_out_gga(X, Y, D)
U6_gga(X, Y, D, gcd_out_gga(s(X), Z, D)) → gcd_le_out_gga(s(X), Y, D)
U2_gga(X, Y, D, gcd_le_out_gga(X, Y, D)) → gcd_out_gga(X, Y, D)
ADD_IN_GAG(s(X), Y, s(Z)) → ADD_IN_GAG(X, Y, Z)
ADD_IN_GAG(s(X), s(Z)) → ADD_IN_GAG(X, Z)
From the DPs we obtained the following set of size-change graphs:
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
gcd_in_gga(X, Y, D) → U1_gga(X, Y, D, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg(0, s(Y))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(X, Y, D, le_out_gg(X, Y)) → U2_gga(X, Y, D, gcd_le_in_gga(X, Y, D))
gcd_le_in_gga(0, Y, Y) → gcd_le_out_gga(0, Y, Y)
gcd_le_in_gga(s(X), Y, D) → U5_gga(X, Y, D, add_in_gag(s(X), Z, Y))
add_in_gag(s(X), Y, s(Z)) → U9_gag(X, Y, Z, add_in_gag(X, Y, Z))
add_in_gag(0, X, X) → add_out_gag(0, X, X)
U9_gag(X, Y, Z, add_out_gag(X, Y, Z)) → add_out_gag(s(X), Y, s(Z))
U5_gga(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_gga(X, Y, D, gcd_in_gga(s(X), Z, D))
gcd_in_gga(X, Y, D) → U3_gga(X, Y, D, gt_in_gg(X, Y))
gt_in_gg(s(X), s(Y)) → U7_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg(s(X), 0)
U7_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(X, Y, D, gt_out_gg(X, Y)) → U4_gga(X, Y, D, gcd_le_in_gga(Y, X, D))
U4_gga(X, Y, D, gcd_le_out_gga(Y, X, D)) → gcd_out_gga(X, Y, D)
U6_gga(X, Y, D, gcd_out_gga(s(X), Z, D)) → gcd_le_out_gga(s(X), Y, D)
U2_gga(X, Y, D, gcd_le_out_gga(X, Y, D)) → gcd_out_gga(X, Y, D)
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
LE_IN_GG(s(X), s(Y)) → LE_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
U1_GGA(X, Y, D, le_out_gg(X, Y)) → GCD_LE_IN_GGA(X, Y, D)
GCD_LE_IN_GGA(s(X), Y, D) → U5_GGA(X, Y, D, add_in_gag(s(X), Z, Y))
U5_GGA(X, Y, D, add_out_gag(s(X), Z, Y)) → GCD_IN_GGA(s(X), Z, D)
GCD_IN_GGA(X, Y, D) → U1_GGA(X, Y, D, le_in_gg(X, Y))
GCD_IN_GGA(X, Y, D) → U3_GGA(X, Y, D, gt_in_gg(X, Y))
U3_GGA(X, Y, D, gt_out_gg(X, Y)) → GCD_LE_IN_GGA(Y, X, D)
gcd_in_gga(X, Y, D) → U1_gga(X, Y, D, le_in_gg(X, Y))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg(0, s(Y))
le_in_gg(0, 0) → le_out_gg(0, 0)
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U1_gga(X, Y, D, le_out_gg(X, Y)) → U2_gga(X, Y, D, gcd_le_in_gga(X, Y, D))
gcd_le_in_gga(0, Y, Y) → gcd_le_out_gga(0, Y, Y)
gcd_le_in_gga(s(X), Y, D) → U5_gga(X, Y, D, add_in_gag(s(X), Z, Y))
add_in_gag(s(X), Y, s(Z)) → U9_gag(X, Y, Z, add_in_gag(X, Y, Z))
add_in_gag(0, X, X) → add_out_gag(0, X, X)
U9_gag(X, Y, Z, add_out_gag(X, Y, Z)) → add_out_gag(s(X), Y, s(Z))
U5_gga(X, Y, D, add_out_gag(s(X), Z, Y)) → U6_gga(X, Y, D, gcd_in_gga(s(X), Z, D))
gcd_in_gga(X, Y, D) → U3_gga(X, Y, D, gt_in_gg(X, Y))
gt_in_gg(s(X), s(Y)) → U7_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg(s(X), 0)
U7_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
U3_gga(X, Y, D, gt_out_gg(X, Y)) → U4_gga(X, Y, D, gcd_le_in_gga(Y, X, D))
U4_gga(X, Y, D, gcd_le_out_gga(Y, X, D)) → gcd_out_gga(X, Y, D)
U6_gga(X, Y, D, gcd_out_gga(s(X), Z, D)) → gcd_le_out_gga(s(X), Y, D)
U2_gga(X, Y, D, gcd_le_out_gga(X, Y, D)) → gcd_out_gga(X, Y, D)
U1_GGA(X, Y, D, le_out_gg(X, Y)) → GCD_LE_IN_GGA(X, Y, D)
GCD_LE_IN_GGA(s(X), Y, D) → U5_GGA(X, Y, D, add_in_gag(s(X), Z, Y))
U5_GGA(X, Y, D, add_out_gag(s(X), Z, Y)) → GCD_IN_GGA(s(X), Z, D)
GCD_IN_GGA(X, Y, D) → U1_GGA(X, Y, D, le_in_gg(X, Y))
GCD_IN_GGA(X, Y, D) → U3_GGA(X, Y, D, gt_in_gg(X, Y))
U3_GGA(X, Y, D, gt_out_gg(X, Y)) → GCD_LE_IN_GGA(Y, X, D)
add_in_gag(s(X), Y, s(Z)) → U9_gag(X, Y, Z, add_in_gag(X, Y, Z))
le_in_gg(s(X), s(Y)) → U8_gg(X, Y, le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg(0, s(Y))
le_in_gg(0, 0) → le_out_gg(0, 0)
gt_in_gg(s(X), s(Y)) → U7_gg(X, Y, gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg(s(X), 0)
U9_gag(X, Y, Z, add_out_gag(X, Y, Z)) → add_out_gag(s(X), Y, s(Z))
U8_gg(X, Y, le_out_gg(X, Y)) → le_out_gg(s(X), s(Y))
U7_gg(X, Y, gt_out_gg(X, Y)) → gt_out_gg(s(X), s(Y))
add_in_gag(0, X, X) → add_out_gag(0, X, X)
U1_GGA(X, Y, le_out_gg) → GCD_LE_IN_GGA(X, Y)
GCD_LE_IN_GGA(s(X), Y) → U5_GGA(X, add_in_gag(s(X), Y))
U5_GGA(X, add_out_gag(Z)) → GCD_IN_GGA(s(X), Z)
GCD_IN_GGA(X, Y) → U1_GGA(X, Y, le_in_gg(X, Y))
GCD_IN_GGA(X, Y) → U3_GGA(X, Y, gt_in_gg(X, Y))
U3_GGA(X, Y, gt_out_gg) → GCD_LE_IN_GGA(Y, X)
add_in_gag(s(X), s(Z)) → U9_gag(add_in_gag(X, Z))
le_in_gg(s(X), s(Y)) → U8_gg(le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg
le_in_gg(0, 0) → le_out_gg
gt_in_gg(s(X), s(Y)) → U7_gg(gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg
U9_gag(add_out_gag(Y)) → add_out_gag(Y)
U8_gg(le_out_gg) → le_out_gg
U7_gg(gt_out_gg) → gt_out_gg
add_in_gag(0, X) → add_out_gag(X)
add_in_gag(x0, x1)
le_in_gg(x0, x1)
gt_in_gg(x0, x1)
U9_gag(x0)
U8_gg(x0)
U7_gg(x0)
U9_gag(add_out_gag(Y)) → add_out_gag(Y)
POL(0) = 0
POL(GCD_IN_GGA(x1, x2)) = 1 + x1 + x2
POL(GCD_LE_IN_GGA(x1, x2)) = 1 + x1 + x2
POL(U1_GGA(x1, x2, x3)) = 1 + x1 + x2
POL(U3_GGA(x1, x2, x3)) = 1 + x1 + x2
POL(U5_GGA(x1, x2)) = x1 + x2
POL(U7_gg(x1)) = 0
POL(U8_gg(x1)) = 0
POL(U9_gag(x1)) = 1 + x1
POL(add_in_gag(x1, x2)) = 2 + x2
POL(add_out_gag(x1)) = 2 + x1
POL(gt_in_gg(x1, x2)) = 0
POL(gt_out_gg) = 0
POL(le_in_gg(x1, x2)) = 0
POL(le_out_gg) = 0
POL(s(x1)) = 1 + x1
U1_GGA(X, Y, le_out_gg) → GCD_LE_IN_GGA(X, Y)
GCD_LE_IN_GGA(s(X), Y) → U5_GGA(X, add_in_gag(s(X), Y))
U5_GGA(X, add_out_gag(Z)) → GCD_IN_GGA(s(X), Z)
GCD_IN_GGA(X, Y) → U1_GGA(X, Y, le_in_gg(X, Y))
GCD_IN_GGA(X, Y) → U3_GGA(X, Y, gt_in_gg(X, Y))
U3_GGA(X, Y, gt_out_gg) → GCD_LE_IN_GGA(Y, X)
add_in_gag(s(X), s(Z)) → U9_gag(add_in_gag(X, Z))
le_in_gg(s(X), s(Y)) → U8_gg(le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg
le_in_gg(0, 0) → le_out_gg
gt_in_gg(s(X), s(Y)) → U7_gg(gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg
U8_gg(le_out_gg) → le_out_gg
U7_gg(gt_out_gg) → gt_out_gg
add_in_gag(0, X) → add_out_gag(X)
add_in_gag(x0, x1)
le_in_gg(x0, x1)
gt_in_gg(x0, x1)
U9_gag(x0)
U8_gg(x0)
U7_gg(x0)
GCD_LE_IN_GGA(s(x0), s(x1)) → U5_GGA(x0, U9_gag(add_in_gag(x0, x1)))
U1_GGA(X, Y, le_out_gg) → GCD_LE_IN_GGA(X, Y)
U5_GGA(X, add_out_gag(Z)) → GCD_IN_GGA(s(X), Z)
GCD_IN_GGA(X, Y) → U1_GGA(X, Y, le_in_gg(X, Y))
GCD_IN_GGA(X, Y) → U3_GGA(X, Y, gt_in_gg(X, Y))
U3_GGA(X, Y, gt_out_gg) → GCD_LE_IN_GGA(Y, X)
GCD_LE_IN_GGA(s(x0), s(x1)) → U5_GGA(x0, U9_gag(add_in_gag(x0, x1)))
add_in_gag(s(X), s(Z)) → U9_gag(add_in_gag(X, Z))
le_in_gg(s(X), s(Y)) → U8_gg(le_in_gg(X, Y))
le_in_gg(0, s(Y)) → le_out_gg
le_in_gg(0, 0) → le_out_gg
gt_in_gg(s(X), s(Y)) → U7_gg(gt_in_gg(X, Y))
gt_in_gg(s(X), 0) → gt_out_gg
U8_gg(le_out_gg) → le_out_gg
U7_gg(gt_out_gg) → gt_out_gg
add_in_gag(0, X) → add_out_gag(X)
add_in_gag(x0, x1)
le_in_gg(x0, x1)
gt_in_gg(x0, x1)
U9_gag(x0)
U8_gg(x0)
U7_gg(x0)